A, B:Type, f:(A(B + Top)), P:(A), p:(x:A. Dec(P(x))), x:A.
(can-apply(p-restrict(f;p);x))  ((can-apply(f;x)) & P(x)) 

latex

ProofTree

Definitions	Type, , x:A. B(x), x(s), t  T, True, x:AB(x), P  Q, P  Q, x. t(x), f(a), T, Top, left + right, p-filter(f), do-apply(f;x), can-apply(f;x), , b, x:A  B(x), P & Q, P  Q, A, Dec(P), if b then t else f fi , Unit, ff, tt, case b of inl(x) => s(x) | inr(y) => t(y), A c B, inr x , inl x , False, s = t, p-restrict(f;p)
Lemmas	iff functionality wrt iff, can-apply-compose-iff, do-apply wf, btrue wf, bfalse wf, can-apply-p-filter, assert wf, can-apply wf, do-apply-p-filter